Issue821.agda:26,9-10
x != (f _ x) of type (D A)
when checking that the expression p has type P (f _ x)
